EDA systems that are known in the art receive high-level behavioral descriptions of an integrated circuit (IC) device and translate them into netlists. The behavioral description is typically expressed in a hardware description languages, such as VHDL or Verilog®. The netlist describes the IC design as a graph, with nodes representing circuit elements and directed edges corresponding to signal lines between the nodes. The netlist can be used to synthesize the actual circuit layout in mask form. Before synthesis, however, the design is generally tested by constructing a software model of the netlist and verifying proper operation by computer simulation and/or formal verification techniques.
“Assertions” are commonly used in circuit design verification. An assertion, in the context of the present description and in the claims, is a statement that validates an assumption or checks a condition that applies to operation of the design being verified. Typically, an assertion is a statement that a certain property is required to be true, for example, that a read_request must always be followed by a read_grant within two clock cycles. Assertions form the basis for automated checking that specified properties are true, and can be used to generate automatic error messages when a given property is violated.
Industry organizations have defined standardized assertion languages that designers can use to specify their assertions, and vendors of EDA systems have developed automated checking tools that integrate these assertions into their simulation environments. For example, the SystemVerilog hardware description language defines SystemVerilog Assertions (SVAs), which can be used in testing circuit designs that are written using Verilog or SystemVerilog. SystemVerilog Assertions are defined and specified in Chapter 16 of the IEEE Standard for SystemVerilog—Unified Hardware Design, Specification and Verification Language (IEEE Std 1800™-2012, February 2013), which is incorporated herein by reference.
U.S. Pat. No. 7,143,373 describes methods and apparatus for evaluating and debugging assertions, including SystemVerilog Assertions. Assertion expressions are evaluated against the binary signal values of a circuit simulation in such a way as to be able to report status information at intermediate levels of assertion subexpressions. In one embodiment, the status information reported for an intermediate subexpression contains the final status of that subexpression in response to a given assertion attempt, at least to the extent it has been determined by the end of the evaluation period (e.g., pass, fail or indeterminate). In another embodiment, the status information reported for an intermediate subexpression contains a tick-by-tick analysis of the activity within that subexpression. In another embodiment, the status information for a subexpression can also contain a tick-by-tick analysis of the activity of an operator of the subexpression. Other kinds and levels of detail at the subexpression level can be provided in various other embodiments.
U.S. Pat. No. 9,032,377, whose disclosure is incorporated herein by reference, describes a method for efficient parallel computation of dependency problems that can be used in design simulation. The method includes accepting a definition of a computing task, which includes multiple Processing Elements (PEs) having execution dependencies. The computing task is compiled for concurrent execution on a multiprocessor device, by arranging the PEs in a series of two or more invocations of the multiprocessor device, including assigning the PEs to the invocations depending on the execution dependencies. The multiprocessor device is invoked to run software code that executes the series of the invocations, so as to produce a result of the computing task. Further aspects of simulation using parallel processors in execution of processing elements are described in U.S. Pat. No. 9,087,166, whose disclosure is likewise incorporated herein by reference.